(set-logic QF_SLIA)
(declare-const x0 Bool)
(declare-const x2 (Seq Bool))
(declare-const i Int)
(assert (= i (str.to_int (str.from_code (seq.len x2)))))
(assert (not (seq.nth x2 i)))
(assert (>= i 0))
(set-info :status sat)
(check-sat)
